Skip to content
Snippets Groups Projects
Commit e31b81e9 authored by BRUN Lelio's avatar BRUN Lelio
Browse files

format

parent 85a7d54a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/backends/C/c_backend.ml
+ 55
− 51
View file @ e31b81e9
......@@ -37,8 +37,7 @@ let with_main_node machines node f =
| Some m ->
f m
let gen_files
generate_spec_header
let gen_files generate_spec_header
( print_memory_header,
print_alloc_header,
print_spec_header,
......@@ -48,59 +47,59 @@ let gen_files
let destname = !Options.dest_dir ^ "/" ^ basename in
(* Generating H spec file *)
if generate_spec_header then
if generate_spec_header then (
let spec_header_file = destname ^ "_spec.h" in
with_out_file spec_header_file (fun header_fmt ->
print_spec_header header_fmt basename machines dependencies);
(* Generating H memory file *)
let memory_header_file = destname ^ "_memory.h" in
with_out_file memory_header_file (fun header_fmt ->
print_memory_header header_fmt basename machines dependencies);
(* Generating H alloc file *)
let alloc_header_file = destname ^ "_alloc.h" in
(* Could be changed *)
with_out_file alloc_header_file (fun header_fmt ->
print_alloc_header header_fmt basename machines dependencies);
(* Generating Lib C file *)
let source_lib_file = c_or_cpp destname in
with_out_file source_lib_file (fun source_lib_fmt ->
print_lib_c source_lib_fmt basename prog machines dependencies);
(* Generating Main C file *)
let main_node = !Options.main_node in
with_main_node machines main_node (fun m ->
let source_main_file = c_or_cpp (destname ^ "_main") in
with_out_file source_main_file (fun source_main_fmt ->
print_main_c source_main_fmt m basename prog machines dependencies));
(* Generating Mauve files *)
with_main_node machines !Options.mauve (fun m ->
let source_mauve_file = destname ^ "_mauve.hpp" in
with_out_file source_mauve_file (fun source_mauve_fmt ->
(* Header *)
print_mauve_header source_mauve_fmt basename;
(* Shell *)
print_mauve_shell source_mauve_fmt m;
(* Core *)
print_mauve_core source_mauve_fmt m;
(* FSM *)
print_mauve_fsm source_mauve_fmt m));
(* Generating Makefile *)
(* Makefiles: - for the moment two cases 1. Classical Makefile, only when
provided with a main node May contain additional framac eacsl targets 2.
Cmake : 2 files - lustrec-basename.cmake describing all variables - the
main CMakeLists.txt activating the first file - Later option 1 should be
removed *)
(* Case 1 *)
if main_node <> "" then
let makefile_file = destname ^ ".makefile" in
(* Generating H memory file *)
let memory_header_file = destname ^ "_memory.h" in
with_out_file memory_header_file (fun header_fmt ->
print_memory_header header_fmt basename machines dependencies);
(* Generating H alloc file *)
let alloc_header_file = destname ^ "_alloc.h" in
(* Could be changed *)
with_out_file makefile_file (fun makefile_fmt ->
print_makefile basename main_node dependencies makefile_fmt)
with_out_file alloc_header_file (fun header_fmt ->
print_alloc_header header_fmt basename machines dependencies);
(* Generating Lib C file *)
let source_lib_file = c_or_cpp destname in
with_out_file source_lib_file (fun source_lib_fmt ->
print_lib_c source_lib_fmt basename prog machines dependencies);
(* Generating Main C file *)
let main_node = !Options.main_node in
with_main_node machines main_node (fun m ->
let source_main_file = c_or_cpp (destname ^ "_main") in
with_out_file source_main_file (fun source_main_fmt ->
print_main_c source_main_fmt m basename prog machines dependencies));
(* Generating Mauve files *)
with_main_node machines !Options.mauve (fun m ->
let source_mauve_file = destname ^ "_mauve.hpp" in
with_out_file source_mauve_file (fun source_mauve_fmt ->
(* Header *)
print_mauve_header source_mauve_fmt basename;
(* Shell *)
print_mauve_shell source_mauve_fmt m;
(* Core *)
print_mauve_core source_mauve_fmt m;
(* FSM *)
print_mauve_fsm source_mauve_fmt m));
(* Generating Makefile *)
(* Makefiles: - for the moment two cases 1. Classical Makefile, only when
provided with a main node May contain additional framac eacsl targets 2.
Cmake : 2 files - lustrec-basename.cmake describing all variables - the
main CMakeLists.txt activating the first file - Later option 1 should be
removed *)
(* Case 1 *)
if main_node <> "" then
let makefile_file = destname ^ ".makefile" in
(* Could be changed *)
with_out_file makefile_file (fun makefile_fmt ->
print_makefile basename main_node dependencies makefile_fmt))
(* (\* Case 2 *\) *)
(* let cmake_file = "lustrec-" ^ basename ^ ".cmake" in *)
......@@ -134,7 +133,12 @@ let print_c_header basename =
Header.pp_header_from_header header_fmt basename lusic.contents
let translate_to_c generate_c_header basename prog machines dependencies =
let generate_spec_header, header_m, source_m, source_main_m, makefile_m, machines =
let ( generate_spec_header,
header_m,
source_m,
source_main_m,
makefile_m,
machines ) =
let open Options in
match !spec with
| SpecNo ->
......
src/backends/C/c_backend_header.ml
+ 13
− 24
View file @ e31b81e9
......@@ -34,7 +34,6 @@ module EmptyMod = struct
module GhostProto = EmptyGhostProto
let pp_predicates _ _ = ()
let pp_machine_decl_prefix _ _ = ()
let pp_import_arrow fmt () =
......@@ -245,12 +244,13 @@ functor
(* Include once: start *)
let machines' = List.filter (fun m -> not m.mis_contract) machines in
let baseNAME = file_to_module_name basename in
let self_dep = {
local = true;
name = basename;
content = [];
is_stateful = true (* assuming it is stateful *);
}
let self_dep =
{
local = true;
name = basename;
content = [];
is_stateful = true (* assuming it is stateful *);
}
in
fprintf
header_fmt
......@@ -259,11 +259,9 @@ functor
#define _%s_ALLOC@,\
@,\
/* Import header from %s */@,\
%a\
@,\
%a@,\
/* Import memory header from %s */@,\
%a\
@,\
%a@,\
%a%a%a#endif@]@."
(* Print the svn version number and the supported C standard (C90 or
C99) *)
......@@ -275,11 +273,11 @@ functor
basename
pp_import_prototype
self_dep
(* Import the memory header *)
(* Import the memory header *)
basename
pp_import_memory_prototype
self_dep
(* Print dependencies *)
(* Print dependencies *)
(pp_print_list
~pp_open_box:pp_open_vbox0
~pp_prologue:(pp_print_endcut "/* Import dependencies */")
......@@ -406,11 +404,7 @@ functor
let baseNAME = file_to_module_name basename in
fprintf
header_fmt
"@[<v>%a@,\
#ifndef _%s_MEMORY@,\
#define _%s_MEMORY@,\
@,\
%a%a#endif@]@."
"@[<v>%a@,#ifndef _%s_MEMORY@,#define _%s_MEMORY@,@,%a%a#endif@]@."
(* Print the svn version number and the supported C standard (C90 or
C99) *)
pp_print_version
......@@ -438,11 +432,7 @@ functor
let baseNAME = file_to_module_name basename in
fprintf
header_fmt
"@[<v>%a@,\
#ifndef _%s_SPEC@,\
#define _%s_SPEC@,\
@,\
%a#endif@]@."
"@[<v>%a@,#ifndef _%s_SPEC@,#define _%s_SPEC@,@,%a#endif@]@."
(* Print the svn version number and the supported C standard (C90 or
C99) *)
pp_print_version
......@@ -451,7 +441,6 @@ functor
baseNAME
Mod.pp_predicates
machines
end
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
......
src/backends/C/c_backend_main.ml
+ 9
− 10
View file @ e31b81e9
......@@ -18,7 +18,6 @@ open C_backend_common
module Mpfr = Lustrec_mpfr
module type MODIFIERS_MAINSRC = sig
val pp_import_spec_prototype : formatter -> dep_t -> unit
val pp_declare_ghost_state : formatter -> ident -> unit
val pp_ghost_state_parameter : formatter -> unit -> unit
......@@ -26,6 +25,7 @@ module type MODIFIERS_MAINSRC = sig
val pp_main_loop_invariants :
ident -> machine_t list -> formatter -> machine_t -> unit
val pp_main_loop_end :
ident -> machine_t list -> formatter -> machine_t -> unit
end
......@@ -465,21 +465,20 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
()
let pp_main_c main_fmt main_machine basename _prog machines _dependencies =
let self_dep = {
local = true;
name = basename;
content = [];
is_stateful = true (* assuming it is stateful*);
}
let self_dep =
{
local = true;
name = basename;
content = [];
is_stateful = true (* assuming it is stateful*);
}
in
fprintf
main_fmt
"@[<v>%a@,\
#include <stdlib.h>@,\
#include <assert.h>@,\
%a\
%a\
@,\
%a%a@,\
%a@,\
%a\n\
\ @]@."
......
src/backends/C/c_backend_main.mli
+ 1
− 0
View file @ e31b81e9
......@@ -11,6 +11,7 @@ module type MODIFIERS_MAINSRC = sig
val pp_main_loop_invariants :
ident -> machine_t list -> formatter -> machine_t -> unit
val pp_main_loop_end :
ident -> machine_t list -> formatter -> machine_t -> unit
end
......
src/backends/C/c_backend_spec.ml
+ 218
− 202
View file @ e31b81e9
......@@ -903,24 +903,23 @@ let pp_arrow_reset_ghost mem fmt inst =
let contract_of machines m =
match m.mspec.mnode_spec with
| Some spec -> (
match spec with
| Contract c ->
Some c, None
| NodeSpec f -> (
let m_f = find_machine f machines in
match m_f.mspec.mnode_spec with
| Some (Contract c) ->
Some c, Some m_f
| _ ->
None, None))
match spec with
| Contract c ->
Some c, None
| NodeSpec f -> (
let m_f = find_machine f machines in
match m_f.mspec.mnode_spec with
| Some (Contract c) ->
Some c, Some m_f
| _ ->
None, None))
| None ->
None, None
let rename n x = sprintf "%s_%d" x n
let rename_var_decl n vd = { vd with var_id = rename n vd.var_id }
let pp_k_induction_case base m m_c pp_mem_out pp_vars fmt
(n, mem_out) =
let pp_k_induction_case base m m_c pp_mem_out pp_vars fmt (n, mem_out) =
let name = m.mname.node_id in
fprintf
fmt
......@@ -943,52 +942,55 @@ let pp_k_induction_case_def base m (_, m_c, _) fmt n =
let stateless = fst (get_stateless_status m) in
let stateless_c = fst (get_stateless_status m_c) in
let l = List.init (n + 1) Fun.id in
let l_pp = List.concat_map (function
| 0 ->
let pp = pp_reset_set' in
[
fun fmt ->
(if stateless_c then fun fmt (x, _) -> pp fmt x
else pp_and pp pp)
fmt
((name, rename 0 mem), (name_c, rename 0 mem_c))
]
| n' ->
let pp_var_c fmt (out, vd) =
if out && n' < n then pp_true_c_bool fmt ()
else pp_var_decl fmt vd
in
let c_inputs =
List.map
(fun v -> false, rename_var_decl n' v)
m_c.mstep.step_inputs
in
let c_outputs =
List.map
(fun v -> true, rename_var_decl n' v)
m_c.mstep.step_outputs
in
let pp stateless pp_var =
pp_transition_aux
stateless
pp_print_string
pp_print_string
pp_var
in
[
(fun fmt ->
pp stateless pp_var_decl fmt
( name,
List.map (rename_var_decl n') (inputs @ outputs),
rename (n' - 1) mem,
rename n' mem ));
(fun fmt ->
pp stateless_c pp_var_c fmt
( name_c,
c_inputs @ c_outputs,
rename (n' - 1) mem_c,
rename n' mem_c ))
]) l
let l_pp =
List.concat_map
(function
| 0 ->
let pp = pp_reset_set' in
[
(fun fmt ->
(if stateless_c then fun fmt (x, _) -> pp fmt x else pp_and pp pp)
fmt
((name, rename 0 mem), (name_c, rename 0 mem_c)));
]
| n' ->
let pp_var_c fmt (out, vd) =
if out && n' < n then pp_true_c_bool fmt () else pp_var_decl fmt vd
in
let c_inputs =
List.map
(fun v -> false, rename_var_decl n' v)
m_c.mstep.step_inputs
in
let c_outputs =
List.map
(fun v -> true, rename_var_decl n' v)
m_c.mstep.step_outputs
in
let pp stateless pp_var =
pp_transition_aux stateless pp_print_string pp_print_string pp_var
in
[
(fun fmt ->
pp
stateless
pp_var_decl
fmt
( name,
List.map (rename_var_decl n') (inputs @ outputs),
rename (n' - 1) mem,
rename n' mem ));
(fun fmt ->
pp
stateless_c
pp_var_c
fmt
( name_c,
c_inputs @ c_outputs,
rename (n' - 1) mem_c,
rename n' mem_c ));
])
l
in
let l_pp = if base then l_pp else List.tl l_pp in
let pp fmt () =
......@@ -998,8 +1000,7 @@ let pp_k_induction_case_def base m (_, m_c, _) fmt n =
pp_exists
(pp_machine_decl
~ghost:true
(pp_comma_list (fun fmt n ->
pp_print_string fmt (rename n mem_c))))
(pp_comma_list (fun fmt n -> pp_print_string fmt (rename n mem_c))))
pp
fmt
((name_c, l), ())
......@@ -1013,24 +1014,23 @@ let pp_k_induction_case_def base m (_, m_c, _) fmt n =
(pp_locals m_c))
(pp_exists
(fun fmt l ->
fprintf
fmt
"%a@,%a"
(pp_machine_decl
~ghost:true
(pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
pp_print_string fmt (rename (n - 1) mem))))
(name, l)
(pp_locals m)
(List.concat_map (fun n ->
List.map (rename_var_decl n) (inputs @ outputs))
l))
fprintf
fmt
"%a@,%a"
(pp_machine_decl
~ghost:true
(pp_comma_list ~pp_eol:pp_print_comma (fun fmt n ->
pp_print_string fmt (rename (n - 1) mem))))
(name, l)
(pp_locals m)
(List.concat_map
(fun n -> List.map (rename_var_decl n) (inputs @ outputs))
l))
pp)
fmt
( (n, (name, rename n mem)),
( List.tl l, () ) )
((n, (name, rename n mem)), (List.tl l, ()))
let pp_base_case_defs m fmt (_, _, k as c_m_k) =
let pp_base_case_defs m fmt ((_, _, k) as c_m_k) =
let l = List.init (k - 1) succ in
pp_print_list
~pp_open_box:pp_open_vbox0
......@@ -1039,7 +1039,7 @@ let pp_base_case_defs m fmt (_, _, k as c_m_k) =
fmt
l
let pp_inductive_case_def m fmt (_, _, k as c_m_k) =
let pp_inductive_case_def m fmt ((_, _, k) as c_m_k) =
pp_k_induction_case_def false m c_m_k fmt k
let pp_k_induction_lemmas m fmt (_, m_c, k) =
......@@ -1050,45 +1050,44 @@ let pp_k_induction_lemmas m fmt (_, m_c, k) =
~pp_open_box:pp_open_vbox0
~pp_sep:pp_print_cutcut
(fun fmt n ->
let outputs = List.map (rename_var_decl n) m_c.mstep.step_outputs in
pp_lemma
(fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
(pp_forall
(fun fmt () ->
fprintf
fmt
"%a,@;%a"
(pp_machine_decl' ~ghost:true)
(name, mem)
(pp_locals m_c)
outputs)
(pp_implies
(pp_k_induction_case
(n <> k)
m
m_c
pp_print_string
(pp_comma_list pp_var_decl))
(pp_and_l
(fun fmt x ->
pp_equal pp_var_decl pp_print_int fmt (x, 1)))))
fmt
(n, ((), ((n, mem), outputs))))
let outputs = List.map (rename_var_decl n) m_c.mstep.step_outputs in
pp_lemma
(fun fmt n -> fprintf fmt "%s_k_induction_%d" name n)
(pp_forall
(fun fmt () ->
fprintf
fmt
"%a,@;%a"
(pp_machine_decl' ~ghost:true)
(name, mem)
(pp_locals m_c)
outputs)
(pp_implies
(pp_k_induction_case
(n <> k)
m
m_c
pp_print_string
(pp_comma_list pp_var_decl))
(pp_and_l (fun fmt x ->
pp_equal pp_var_decl pp_print_int fmt (x, 1)))))
fmt
(n, ((), ((n, mem), outputs))))
fmt
l
let pp_k_induction m fmt c_m_k =
pp_acsl_cut
(fun fmt () ->
fprintf
fmt
"%a@,@,%a@,@,%a"
(pp_base_case_defs m)
c_m_k
(pp_inductive_case_def m)
c_m_k
(pp_k_induction_lemmas m)
c_m_k)
fprintf
fmt
"%a@,@,%a@,@,%a"
(pp_base_case_defs m)
c_m_k
(pp_inductive_case_def m)
c_m_k
(pp_k_induction_lemmas m)
c_m_k)
fmt
()
......@@ -1145,11 +1144,9 @@ module HdrMod = struct
"/* ACSL transition memory footprints lemmas */"
pp_transition_footprint_lemmas)
machines
(pp_preds
"/* k-induction predicates and lemmas */"
(fun fmt m ->
let c, m_c = contract_of machines m in
pp_print_option (pp_proof_annotation m m_c) fmt c))
(pp_preds "/* k-induction predicates and lemmas */" (fun fmt m ->
let c, m_c = contract_of machines m in
pp_print_option (pp_proof_annotation m m_c) fmt c))
machines
let pp_machine_decl_prefix _ _ = ()
......@@ -1285,7 +1282,8 @@ module SrcMod = struct
(* let rename_predicate n = function *)
(* | Transition (s, f, inst, i, es, r, mf, mif) -> *)
(* Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf, mif) *)
(* Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf,
mif) *)
(* | p -> *)
(* p *)
......@@ -1374,15 +1372,15 @@ module SrcMod = struct
pp_print_string
pp_print_string
(fun fmt v ->
(if is_output m v then pp_ptr_decl else pp_var_decl)
fmt
v)))
(if is_output m v then pp_ptr_decl else pp_var_decl)
fmt
v)))
fmt
( m_c.mstep.step_outputs,
( m_c.mname.node_id,
m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
mem_in,
mem_out )))
m_c.mstep.step_inputs @ m_c.mstep.step_outputs,
mem_in,
mem_out ) ))
fmt
m_c)
in
......@@ -1562,9 +1560,7 @@ module SrcMod = struct
end
module MainMod = struct
let pp_import_spec_prototype = SrcMod.pp_import_spec_prototype
let main_mem_ghost = "main_mem_ghost"
let pp_declare_ghost_state fmt name =
......@@ -1587,94 +1583,114 @@ module MainMod = struct
let k_induction_of machines m =
match contract_of machines m with
| Some c, Some m_c ->
begin match c.mc_proof with
| Some (Kinduction k) ->
Some (m_c, k)
| _ -> None
end
| _ -> None
| Some c, Some m_c -> (
match c.mc_proof with Some (Kinduction k) -> Some (m_c, k) | _ -> None)
| _ ->
None
let pp_main_loop_invariants main_mem machines fmt m =
let name = m.mname.node_id in
let insts = instances machines m in
let m_c_k = k_induction_of machines m in
fprintf fmt "%a%a"
(pp_print_option
(fun fmt _ ->
fprintf fmt "%a@,"
(pp_acsl_line (pp_ghost pp_print_string)) "int __k = 0;"))
fprintf
fmt
"%a%a"
(pp_print_option (fun fmt _ ->
fprintf
fmt
"%a@,"
(pp_acsl_line (pp_ghost pp_print_string))
"int __k = 0;"))
m_c_k
(pp_acsl_cut
(fun fmt () ->
fprintf
fmt
"%a@,%a@,%a@,%a%a"
(pp_loop_invariant pp_mem_valid')
(name, main_mem)
(pp_loop_invariant
(pp_memory_pack_aux pp_print_string pp_print_string))
(name, main_mem_ghost, main_mem)
(pp_loop_invariant
(pp_separated
(pp_paren pp_print_string)
pp_ref'
(pp_ref pp_var_decl)))
(main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
(pp_loop_invariant
(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
((), ((), ()))
(pp_print_option
(fun fmt (m_c, k) ->
fprintf fmt "@,%a@,%a"
(pp_loop_invariant (pp_gequal pp_print_string pp_print_int))
("__k", 0)
(pp_loop_invariant
(pp_and_l (fun fmt k' ->
pp_paren
(pp_implies
((if k' = k then pp_gequal else pp_equal) pp_print_string pp_print_int)
(fun fmt mem ->
if k' = 0 then pp_reset_set' fmt (name, mem)
else pp_k_induction_case
(k' < k)
m
m_c
pp_print_string
(pp_comma_list ~pp_open_box:(fun fmt () -> pp_open_hovbox fmt 0) (fun fmt _ -> pp_true_c_bool fmt ()))
fmt (k', mem)))
fmt
(("__k", k'),
main_mem_ghost))))
(List.init (k + 1) Fun.id)))
m_c_k))
(pp_acsl_cut (fun fmt () ->
fprintf
fmt
"%a@,%a@,%a@,%a%a"
(pp_loop_invariant pp_mem_valid')
(name, main_mem)
(pp_loop_invariant
(pp_memory_pack_aux pp_print_string pp_print_string))
(name, main_mem_ghost, main_mem)
(pp_loop_invariant
(pp_separated
(pp_paren pp_print_string)
pp_ref'
(pp_ref pp_var_decl)))
(main_mem, main_mem_ghost, insts, m.mstep.step_outputs)
(pp_loop_invariant
(pp_or (pp_valid_read pp_stdout) (pp_equal pp_stdout pp_null)))
((), ((), ()))
(pp_print_option (fun fmt (m_c, k) ->
fprintf
fmt
"@,%a@,%a"
(pp_loop_invariant (pp_gequal pp_print_string pp_print_int))
("__k", 0)
(pp_loop_invariant
(pp_and_l (fun fmt k' ->
pp_paren
(pp_implies
((if k' = k then pp_gequal else pp_equal)
pp_print_string
pp_print_int)
(fun fmt mem ->
if k' = 0 then pp_reset_set' fmt (name, mem)
else
pp_k_induction_case
(k' < k)
m
m_c
pp_print_string
(pp_comma_list
~pp_open_box:(fun fmt () ->
pp_open_hovbox fmt 0)
(fun fmt _ -> pp_true_c_bool fmt ()))
fmt
(k', mem)))
fmt
(("__k", k'), main_mem_ghost))))
(List.init (k + 1) Fun.id)))
m_c_k))
()
let pp_main_loop_end _main_mem machines fmt m =
fprintf fmt "@,%a"
(pp_print_option
(fun fmt (m_c, _) ->
let stateless_c = fst (get_stateless_status m_c) in
let name_c = m_c.mname.node_id in
let mem_in_c = mk_mem_in_c m in
let mem_out_c = mk_mem_out_c m in
let pp_var_c fmt (out, vd) =
if out then pp_true_c_bool fmt ()
else pp_var_decl fmt vd
in
let c_inputs = List.map (fun v -> false, v) m_c.mstep.step_inputs in
let c_outputs = List.map (fun v -> true, v) m_c.mstep.step_outputs in
fprintf fmt "%a@,%a"
(pp_acsl_line (pp_ghost pp_print_string))
"__k++;"
(pp_acsl_line'
(pp_assert
(pp_transition_aux
stateless_c
pp_print_string
pp_print_string
pp_var_c)))
(name_c, c_inputs @ c_outputs, mem_in_c, mem_out_c)))
fprintf
fmt
"@,%a"
(pp_print_option (fun fmt (m_c, _) ->
let stateless_c = fst (get_stateless_status m_c) in
let name_c = m_c.mname.node_id in
let mem_in_c = mk_mem_in_c m in
let mem_out_c = mk_mem_out_c m in
let pp_var_c fmt (out, vd) =
if out then pp_true_c_bool fmt () else pp_var_decl fmt vd
in
let c_inputs = List.map (fun v -> false, v) m_c.mstep.step_inputs in
let c_outputs = List.map (fun v -> true, v) m_c.mstep.step_outputs in
let pp =
pp_transition_aux
stateless_c
pp_print_string
pp_print_string
pp_var_c
in
fprintf
fmt
"%a@,%a"
(pp_acsl_line (pp_ghost pp_print_string))
"__k++;"
(pp_acsl_line'
(pp_assert (fun fmt x ->
if stateless_c then pp fmt x
else
pp_exists
(pp_machine_decl
~ghost:true
(pp_comma_list pp_print_string))
pp
fmt
((name_c, [ mem_in_c; mem_out_c ]), x))))
(name_c, c_inputs @ c_outputs, mem_in_c, mem_out_c)))
(k_induction_of machines m)
let pp_main_spec fmt =
......
src/backends/C/c_backend_src.ml
+ 7
− 8
View file @ e31b81e9
......@@ -22,7 +22,6 @@ module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
val pp_import_spec_prototype : formatter -> dep_t -> unit
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
......@@ -33,7 +32,6 @@ module type MODIFIERS_SRC = sig
machine_t -> ident -> ident -> formatter -> instr_t -> unit
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
val pp_c_decl_local_spec_var : machine_t -> formatter -> var_decl -> unit
val get_spec_locals : machine_t -> var_decl list
val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit
......@@ -1001,12 +999,13 @@ module Main (Mod : MODIFIERS_SRC) = struct
ind.nodei_id
let pp_lib_c source_fmt basename prog machines dependencies =
let self_dep = {
local = true;
name = basename;
content = [];
is_stateful = true (* assuming it is stateful *);
}
let self_dep =
{
local = true;
name = basename;
content = [];
is_stateful = true (* assuming it is stateful *);
}
in
fprintf
source_fmt
......
src/backends/C/c_backend_src.mli
+ 0
− 2
View file @ e31b81e9
......@@ -8,7 +8,6 @@ module type MODIFIERS_SRC = sig
module GhostProto : MODIFIERS_GHOST_PROTO
val pp_import_spec_prototype : formatter -> dep_t -> unit
val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
......@@ -19,7 +18,6 @@ module type MODIFIERS_SRC = sig
machine_t -> ident -> ident -> formatter -> instr_t -> unit
val pp_ghost_parameter : ident -> formatter -> ident option -> unit
val pp_c_decl_local_spec_var : machine_t -> formatter -> var_decl -> unit
val get_spec_locals : machine_t -> var_decl list
val pp_ghost_reset_memory : machine_t -> formatter -> ident -> unit
......
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