Skip to content
Snippets Groups Projects
Commit b0eb180d authored by Thibault Martin's avatar Thibault Martin Committed by Allan Blanchard
Browse files

Also generate assigns from prototype for definitions

parent 4e5130cb
No related branches found
No related tags found
No related merge requests found
...@@ -354,9 +354,8 @@ struct ...@@ -354,9 +354,8 @@ struct
else WritesAny else WritesAny
let frama_c_default kf = let frama_c_default kf =
if Kernel_function.has_definition kf then (* TODO: use genassigns for Definitions. *)
acsl_default () (* TODO: use genassigns *) Writes (Infer_annotations.assigns_from_prototype kf)
else Writes (Infer_annotations.assigns_from_prototype kf)
let compare_deps d1 d2 = let compare_deps d1 d2 =
match d1, d2 with match d1, d2 with
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment