diff --git a/examples/real/safety/model.aadl.out b/examples/real/safety/model.aadl.out index 464290ad9671446e10f603bb859435325f9c57e3..a91d796944abf38e9826929ed2cd851905ce0ffb 100644 --- a/examples/real/safety/model.aadl.out +++ b/examples/real/safety/model.aadl.out @@ -23,4 +23,4 @@ libsafety.real:32:46 Backends: error : Property is false for instance 69 (node.i theorem check_error_handling is: FALSE -model.aadl:118:07 Backends: fatal error : requirements are not fulfilled +model.aadl:118:07 Backends: fatal error : requirements are not fulfilled for theorem pok_safety diff --git a/src/backends/ocarina-backends-real.adb b/src/backends/ocarina-backends-real.adb index 72b2100fe5b059255099bf7cd1de73372613592c..df7bb2c556103f0ceb934dcbc713a3437a82f53b 100644 --- a/src/backends/ocarina-backends-real.adb +++ b/src/backends/ocarina-backends-real.adb @@ -526,7 +526,7 @@ package body Ocarina.Backends.REAL is if not Check_Requirements (RNU.REAL_Root) then Display_Located_Error (Loc (RNU.REAL_Root), "requirements are not fulfilled", - Fatal => True); + Fatal => not Ocarina.Analyzer.REAL.Continue_Evaluation); end if; -- Library theorems are already analyzed, so we proceed @@ -686,7 +686,7 @@ package body Ocarina.Backends.REAL is if not Check_Requirements (RNU.REAL_Root) then Display_Located_Error (Loc (RNU.REAL_Root), "requirements are not fulfilled", - Fatal => True); + Fatal => not Ocarina.Analyzer.REAL.Continue_Evaluation); end if; Initialize_Sets_Table (RNU.REAL_Root); @@ -850,7 +850,6 @@ package body Ocarina.Backends.REAL is Compute_Check_Expression (D, Ret, Result); if Ret = RT_Error then - Display_Located_Error (Loc (D), "o<", Fatal => False); return False; elsif Ret = RT_Boolean then @@ -3083,8 +3082,16 @@ package body Ocarina.Backends.REAL is if not Check_Requirements (RNU.REAL_Root) then Display_Located_Error - (Loc (RNU.REAL_Root), "requirements are not fulfilled", - Fatal => True); + (Loc (RNU.REAL_Root), + "requirements are not fulfilled for theorem " + & Get_Name_String (RN.Name (RN.Identifier (RNU.REAL_Root))), + Fatal => not Ocarina.Analyzer.REAL.Continue_Evaluation); + Write_Line (""); + Write_Line + ("theorem " + & Get_Name_String (RN.Name (RN.Identifier (RNU.REAL_Root))) + & " is: FALSE"); + else Initialize_Sets_Table (RNU.REAL_Root); Apply_To_All_Elements (RNU.REAL_Root); diff --git a/tests/MANIFEST b/tests/MANIFEST index 7390da566f55a7288bfd7e8d05053500ed89d87d..a4ffd48369d1315a86ff2f2d4cc4215aaa9a8f5b 100644 --- a/tests/MANIFEST +++ b/tests/MANIFEST @@ -250,6 +250,7 @@ tests/real-annexes-execution/test_real_exec_05.aadl tests/real-annexes-execution/test_real_exec_06.aadl tests/real-annexes-execution-environment/test_real_exec_env_01.aadl tests/real_units/validation.aadl +tests/real_requires/test.aadl tests/ticket_46/test.aadl tests/ticket_48/test.aadl diff --git a/tests/real_requires/MANIFEST b/tests/real_requires/MANIFEST new file mode 100644 index 0000000000000000000000000000000000000000..5eab743783560dbf0e689c311bcb550e855fa26d --- /dev/null +++ b/tests/real_requires/MANIFEST @@ -0,0 +1,3 @@ +AADL_VERSION=-aadlv2 +OCARINA_FLAGS=-q -real_continue_eval -g real_theorem -real_lib theorems.real -r a.impl + diff --git a/tests/real_requires/test.aadl b/tests/real_requires/test.aadl new file mode 100644 index 0000000000000000000000000000000000000000..0278b24e3057dc1c05cdc741de383c60d08f690f --- /dev/null +++ b/tests/real_requires/test.aadl @@ -0,0 +1,22 @@ +package Test +public + +system A +end A; + +system implementation A.impl +annex real_specification {** + theorem test_theorem + foreach s in system_set do + requires(required_theorem); + check(1=1); + end test_theorem; + + theorem test_theorem2 + foreach s in system_set do + check(1=1); + end test_theorem2; +**}; +end A.impl; + +end Test; \ No newline at end of file diff --git a/tests/real_requires/test.aadl.out b/tests/real_requires/test.aadl.out new file mode 100644 index 0000000000000000000000000000000000000000..d2faae41f3cc602f50a4f28603ab87dfadead2c0 --- /dev/null +++ b/tests/real_requires/test.aadl.out @@ -0,0 +1,25 @@ +test_theorem execution +requirement : required_theorem +------------------------------------- +Evaluating theorem required_theorem + + * Iterate for variable: a.impl +theorems.real:3:09 Backends: error : Property is false for instance 6 (a.impl) + => Result: FALSE + +theorem required_theorem is: FALSE + +test.aadl:9:02 Backends: error : requirements are not fulfilled for theorem test_theorem + +theorem test_theorem is: FALSE + +test_theorem2 execution +------------------------------------- +Evaluating theorem test_theorem2 + + * Iterate for variable: a.impl + => Result: TRUE + +theorem test_theorem2 is: TRUE + + diff --git a/tests/real_requires/theorems.real b/tests/real_requires/theorems.real new file mode 100644 index 0000000000000000000000000000000000000000..379bea53c7dfe6f1eb7c16a50d7ed3090235f49a --- /dev/null +++ b/tests/real_requires/theorems.real @@ -0,0 +1,4 @@ +theorem required_theorem +foreach s in system_set do + check(1=0); +end required_theorem;