Commit 7f41e2e0 authored by jhugues's avatar jhugues

* Do not exit immediately if a requirement is not fulfilled

          and -real_continue_eval has been selected



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@5005 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent 3917856c
......@@ -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
......@@ -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);
......
......@@ -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
......
AADL_VERSION=-aadlv2
OCARINA_FLAGS=-q -real_continue_eval -g real_theorem -real_lib theorems.real -r a.impl
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
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
theorem required_theorem
foreach s in system_set do
check(1=0);
end required_theorem;
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