Commit ab49e183 authored by Julien Signoles's avatar Julien Signoles
Browse files

fix compilation according to kernel changes

parent 1c2227d4
......@@ -57,13 +57,14 @@ let unmemoized_extend_ast () =
(Kernel.Machdep.get ())
Config.datadir);
Kernel.Keep_unused_specified_functions.off ();
let ppc, ppk = File.get_preprocessor_command () in
let register s =
let cpp =
fst (File.get_preprocessor_command ()) ^
Pretty_utils.sfprintf
" -I%s" (Options.Share.dir ~error:true ())
in
File.pre_register (File.from_filename ~cpp s)
File.pre_register
(File.NeedCPP
(s,
ppc
^ Pretty_utils.sfprintf " -I%s" (Options.Share.dir ~error:true ()),
ppk))
in
List.iter register (Misc.library_files ())
in
......
......@@ -323,7 +323,7 @@ module rec Transfer
| Pfreeable _ -> Error.not_yet "\\freeable"
| Pfresh _ -> Error.not_yet "\\fresh"
| Pseparated _ -> Error.not_yet "\\separated"
| Pspecified _ -> Error.not_yet "\\specified"
| Pdangling _ -> Error.not_yet "\\dangling"
| Ptrue | Pfalse | Papp _ | Prel _
| Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
| Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
......
......@@ -563,7 +563,7 @@ and named_predicate_content_to_exp ?name kf env p =
| Ptrue -> Cil.one ~loc, env
| Papp _ -> not_yet env "logic function application"
| Pseparated _ -> not_yet env "\\separated"
| Pspecified _ -> not_yet env "\\specified"
| Pdangling _ -> not_yet env "\\dangling"
| Prel(rel, t1, t2) ->
let e, env =
comparison_to_exp ~loc kf env (relation_to_binop rel) t1 t2 None
......
......@@ -441,7 +441,7 @@ let rec type_predicate_named p =
| Pfalse | Ptrue -> ()
| Papp _ -> Error.not_yet "logic function application"
| Pseparated _ -> Error.not_yet "\\separated"
| Pspecified _ -> Error.not_yet "\\specified"
| Pdangling _ -> Error.not_yet "\\dangling"
| Prel(_, t1, t2) ->
ignore (type_term t1);
ignore (type_term t2)
......
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