diff options
Diffstat (limited to 'driver/Interp.ml')
| -rw-r--r-- | driver/Interp.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index f453af95..fb1c85f0 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -59,7 +59,7 @@ let print_eventval_list p = function let print_event p = function | Event_syscall(id, args, res) -> fprintf p "extcall %s(%a) -> %a" - (extern_atom id) + (camlstring_of_coqstring id) print_eventval_list args print_eventval res | Event_vload(chunk, id, ofs, res) -> @@ -74,7 +74,7 @@ let print_event p = function print_eventval arg | Event_annot(text, args) -> fprintf p "annotation \"%s\" %a" - (extern_atom text) + (camlstring_of_coqstring text) print_eventval_list args (* Printing states *) @@ -98,7 +98,7 @@ let name_of_function prog fn = in find_name prog.prog_defs let invert_local_variable e b = - Maps.PTree.fold + Maps.PTree.fold (fun res id (b', _) -> if b = b' then Some id else res) e None @@ -176,7 +176,7 @@ let rec compare_cont k1 k2 = match k1, k2 with | Kstop, Kstop -> 0 | Kdo k1, Kdo k2 -> compare_cont k1 k2 - | Kseq(s1, k1), Kseq(s2, k2) -> + | Kseq(s1, k1), Kseq(s2, k2) -> let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2 | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) -> let c = compare (s1,s1') (s2,s2') in @@ -273,7 +273,7 @@ let extract_string m blk ofs = if c = '\000' then begin Some(Buffer.contents b) end else begin - Buffer.add_char b c; + Buffer.add_char b c; extract blk (Z.succ ofs) end | _ -> @@ -325,7 +325,7 @@ let format_value m flags length conv arg = | 'p', "", _ -> "<int or pointer argument expected>" | _, _, _ -> - "<unrecognized format>" + "<unrecognized format>" let do_printf m fmt args = @@ -374,7 +374,7 @@ let convert_external_arg ge v t = | Vfloat f, AST.Tfloat -> Some (EVfloat f) | Vsingle f, AST.Tsingle -> Some (EVsingle f) | Vlong n, AST.Tlong -> Some (EVlong n) - | Vptr(b, ofs), AST.Tint -> + | Vptr(b, ofs), AST.Tint -> Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) | _, _ -> None @@ -387,7 +387,7 @@ let rec convert_external_args ge vl tl = | _, _ -> None let do_external_function id sg ge w args m = - match extern_atom id, args with + match camlstring_of_coqstring id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); @@ -565,7 +565,7 @@ let rec explore_all p prog ge time states = if nextstates <> [] then explore_all p prog ge (time + 1) nextstates (* The variant of the source program used to build the world for - executing events. + executing events. Volatile variables are turned into non-volatile ones, so that reads and writes can be performed. Other variables are turned into empty vars, so that |