Merge branch 'feature/annotate_assembly' into 'master'

Feature/annotate assembly

Branch compatible with Frama-C branch of the same name (MR 486).

See merge request !22

src/plugins/e-acsl/dup_functions.ml

@@ -92,8 +92,8 @@ let copy_ppt old_prj new_prj old_ppt new_ppt =
 (* ********************************************************************** *)
 
 let dup_spec_status old_prj kf new_kf old_spec new_spec =
-  let old_ppts = Property.ip_of_spec kf Kglobal old_spec in
-  let new_ppts = Property.ip_of_spec new_kf Kglobal new_spec in
+  let old_ppts = Property.ip_of_spec kf Kglobal ~active:[] old_spec in
+  let new_ppts = Property.ip_of_spec new_kf Kglobal ~active:[] new_spec in
   List.iter2 (copy_ppt old_prj (Project.current ())) old_ppts new_ppts
 
 let dup_funspec tbl bhv spec =

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle

@@ -24,10 +24,10 @@ tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.

src/plugins/e-acsl/translate.ml

@@ -853,20 +853,20 @@ let translate_pre_spec kf kinstr env spec =
     | [] -> ()
     | l ->
       unsupported
-	(List.iter
-	   (fun l ->
-	     if must_translate (Property.ip_of_complete kf kinstr l) then
-	       not_yet env "complete behaviors"))
-	l);
+        (List.iter
+           (fun l ->
+             if must_translate (Property.ip_of_complete kf kinstr ~active:[] l)
+             then not_yet env "complete behaviors"))
+        l);
     (match spec.spec_disjoint_behaviors with
     | [] -> ()
     | l ->
       unsupported
-	(List.iter
-	   (fun l ->
-	     if must_translate (Property.ip_of_disjoint kf kinstr l) then
-	       not_yet env "disjoint behaviors"))
-	l);
+        (List.iter
+           (fun l ->
+             if must_translate (Property.ip_of_disjoint kf kinstr ~active:[] l)
+             then not_yet env "disjoint behaviors"))
+        l);
     env
   in
   let env = convert_unsupported_clauses env in