Commit 5e135627 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/kernel/check-assertion' into 'master'

Synchronize with frama-c!2182: new assertion kind, assert or check.

See merge request frama-c/e-acsl!285
parents 77667c71 265122cc
......@@ -49,7 +49,7 @@ let search_assert_or_invariant kf =
Annotations.iter_all_code_annot
(fun stmt _ a ->
match a.annot_content with
| AAssert(_, p) | AInvariant(_, _, p) ->
| AAssert(_, _, p) | AInvariant(_, _, p) ->
let line = Ppt_line.get () in
if (fst (p.loc)).Lexing.pos_lnum = line then
raise (Found(Property.ip_of_code_annot_single kf stmt a, line))
......
......@@ -798,7 +798,7 @@ and translate_rte_annots:
let env =
List.fold_left
(fun env a -> match a.annot_content with
| AAssert(_, p) ->
| AAssert(_, _, p) ->
handle_error
(fun env ->
Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
......@@ -1018,7 +1018,7 @@ let translate_post_spec kf env spec =
let translate_pre_code_annotation kf env annot =
let convert env = match annot.annot_content with
| AAssert(l, p) ->
| AAssert(l, _, p) ->
if Keep_status.must_translate kf Keep_status.K_Assert then
let env = Env.set_annotation_kind env Misc.Assertion in
if l <> [] then
......
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