Skip to content
Snippets Groups Projects
Commit 21615c0f authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Fix location on funspec unsupported clauses messages

parent abd17210
No related branches found
No related tags found
No related merge requests found
......@@ -67,8 +67,9 @@ let pre_funspec kf kinstr env funspec =
funspec;
env
in
let env = convert_unsupported_clauses env in
let loc = Kernel_function.get_location kf in
Cil.CurrentLoc.set loc;
let env = convert_unsupported_clauses env in
let contract = Contract.create ~loc funspec in
Env.with_rte env true
~f:(fun env -> Contract.translate_preconditions kf kinstr env contract)
......
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