Commit 235ac7f3 authored by jhugues's avatar jhugues
Browse files

* When a requirement for a theorem is not met, propagate the

          error to caller theorem

git-svn-id: 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent f7365b8e
......@@ -532,13 +532,14 @@ package body Ocarina.Backends.REAL is
(Loc (RNU.REAL_Root), "requirements are not fulfilled",
Fatal => not Ocarina.Analyzer.REAL.Continue_Evaluation);
Success := False;
end if;
-- Library theorems are already analyzed, so we proceed
-- directly to execution
Initialize_Sets_Table (RNU.REAL_Root);
Success := Apply_To_All_Elements (RNU.REAL_Root);
Success := Apply_To_All_Elements (RNU.REAL_Root) and then Success;
exit when (not Success)
......@@ -685,6 +686,7 @@ package body Ocarina.Backends.REAL is
-- 3/ Initialize the runtime space with new values
-- Library theorems are already analyzed
-- so we proceed directly to execution
REAL_Root := Related_Theorem (E);
......@@ -696,7 +698,7 @@ package body Ocarina.Backends.REAL is
Initialize_Sets_Table (RNU.REAL_Root);
-- 4/ Launch the extern theorem
-- 4/ Launch the external theorem
Compute_Value (RNU.REAL_Root, Success, R);
if not Success then
......@@ -251,6 +251,7 @@ tests/real-annexes-execution/test_real_exec_06.aadl
OCARINA_FLAGS=-q -real_continue_eval -g real_theorem -real_lib theorems.real -r a.impl
package BugTest
system A
end A;
system implementation A.impl
annex real_specification {**
theorem test
foreach s in system_set do
requires (sub1);
check (1 = 1);
end test;
end A.impl;
end BugTest;
test execution
requirement : sub1
requirement : sub2
Evaluating theorem sub2
* Iterate for variable: a.impl
theorems.real:9:10 Backends: error : Property is false for instance 6 (a.impl)
=> Result: FALSE
theorem sub2 is: FALSE
theorems.real:1:01 Backends: error : requirements are not fulfilled
Evaluating theorem sub1
* Iterate for variable: a.impl
=> Result: TRUE
theorem sub1 is: TRUE
test.aadl:8:05 Backends: error : requirements are not fulfilled for theorem test
theorem test is: FALSE
theorem sub1
foreach s in System_Set do
check (1 = 1);
end sub1;
theorem sub2
foreach s in System_Set do
check (1 = 0);
end sub2;
Supports Markdown
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