Skip to content

GitLab

Commit 4d26965d authored by yoogx's avatar yoogx
Browse files

* Added targets to support use of GNATPRove from project files 

          and makefile generated for PolyORB-HI/Ada
parent 01b2d3f3
Hide whitespace changes
Inline Side-by-side
src/backends/ocarina-backends-build_utils.adb
View file @ 4d26965d
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2013 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the --
......@@ -1585,6 +1585,11 @@ package body Ocarina.Backends.Build_Utils is
Compile_Ada_Files (M.Ada_Sources);
Write_Eol;
Write_Line ("prove:");
Write_Line (ASCII.HT
& "gnatprove -P$(PROJECT_FILE) --warnings=continue "
& "--report=fail");
-- Close the file
Close (Fd);
......
src/backends/ocarina-backends-po_hi_ada.adb
View file @ 4d26965d
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2012 ESA & ISAE. --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2014 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify --
-- it under terms of the GNU General Public License as published by the --
......@@ -493,6 +493,8 @@ package body Ocarina.Backends.PO_HI_Ada is
Write_Line ("package Linker renames PolyORB_HI.Linker;");
Write_Indentation;
Write_Line ("package Check renames PolyORB_HI.Check;");
Write_Indentation;
Write_Line ("package Prove renames PolyORB_HI.Prove;");
Write_Eol;
Decrement_Indentation;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment