Revision b2ad5de3
Added by Lélio Brun over 3 years ago
| dune | ||
|---|---|---|
| 51 | 51 |
cmake |
| 52 | 52 |
"-DSUBPROJ=\"unstable\"" |
| 53 | 53 |
"-DLUSTRE_INCLUDE_DIR=%{project_root}/include"
|
| 54 |
"-DLUSTRE_COMPILER=%{bin:lustrec}"
|
|
| 54 | 55 |
.) |
| 55 | 56 |
(run |
| 56 | 57 |
ctest |
| ... | ... | |
| 59 | 60 |
-R |
| 60 | 61 |
"COMPIL_LUS|MAKE|BIN|DIFF" |
| 61 | 62 |
-E |
| 62 |
LUSTRET |
|
| 63 |
--progress))))) |
|
| 63 |
LUSTRET) |
|
| 64 |
)))) |
|
| src/backends/C/c_backend_common.ml | ||
|---|---|---|
| 1210 | 1210 |
eprintf "Internal error: C_backend_common.pp_static_val"; |
| 1211 | 1211 |
assert false |
| 1212 | 1212 |
|
| 1213 |
let concat x y = |
|
| 1214 |
x ^ "##" ^ y |
|
| 1215 |
|
|
| 1213 | 1216 |
let pp_constant_decl (m, attr, inst) pp_var fmt v = |
| 1214 | 1217 |
fprintf |
| 1215 | 1218 |
fmt |
| 1216 | 1219 |
"%s %a = %a" |
| 1217 | 1220 |
attr |
| 1218 |
(pp_c_type (sprintf "%s ## %s" inst v.var_id))
|
|
| 1221 |
(pp_c_type (concat inst v.var_id))
|
|
| 1219 | 1222 |
v.var_type |
| 1220 | 1223 |
(pp_static_val pp_var) |
| 1221 | 1224 |
(get_const_assign m v) |
| 1222 | 1225 |
|
| 1223 | 1226 |
let pp_var inst const_locals fmt v = |
| 1224 |
if List.mem v const_locals then fprintf fmt "%s ## %s" inst v.var_id |
|
| 1225 |
else fprintf fmt "%s" v.var_id |
|
| 1227 |
pp_print_string fmt (if List.mem v const_locals then concat inst v.var_id else v.var_id) |
|
| 1226 | 1228 |
|
| 1227 | 1229 |
let pp_static_constant_decl ((_, _, inst) as macro) fmt const_locals = |
| 1228 | 1230 |
pp_print_list |
| ... | ... | |
| 1238 | 1240 |
let values = List.map (value_of_dimension m) static in |
| 1239 | 1241 |
fprintf |
| 1240 | 1242 |
fmt |
| 1241 |
"%a(%s, %a%s)"
|
|
| 1243 |
"@[<h>%a(%s, %a%s)@]"
|
|
| 1242 | 1244 |
(pp_machine_static_declare_name ~ghost) |
| 1243 | 1245 |
(node_name n) |
| 1244 | 1246 |
attr |
| ... | ... | |
| 1259 | 1261 |
in |
| 1260 | 1262 |
fprintf |
| 1261 | 1263 |
fmt |
| 1262 |
"@[<v 2>#define %a(%s, %a%s)\\@,%a%s %a %s;\\@,%a%a;@]" |
|
| 1264 |
"@[<v 2>@[<h>#define %a(%s, %a%s)\\@]@,\ |
|
| 1265 |
@[<h>%a%s %a %s;\\@]@,\ |
|
| 1266 |
%a%a;@]" |
|
| 1263 | 1267 |
(pp_machine_static_declare_name ~ghost) |
| 1264 | 1268 |
m.mname.node_id |
| 1265 | 1269 |
attr |
| 1266 | 1270 |
(pp_print_list |
| 1271 |
~pp_open_box:pp_open_hbox |
|
| 1267 | 1272 |
~pp_sep:pp_print_comma |
| 1268 | 1273 |
~pp_eol:pp_print_comma |
| 1269 | 1274 |
(pp_c_var_read m)) |
| ... | ... | |
| 1286 | 1291 |
~pp_open_box:pp_open_vbox0 |
| 1287 | 1292 |
~pp_sep:(pp_print_endcut ";\\") |
| 1288 | 1293 |
(fun fmt (i', m') -> |
| 1289 |
let path = sprintf "%s ## _%s" inst i' in |
|
| 1290 |
fprintf |
|
| 1291 |
fmt |
|
| 1292 |
"%a" |
|
| 1293 |
(pp_static_declare_instance ~ghost macro const_locals) |
|
| 1294 |
(path, m'))) |
|
| 1294 |
let path = concat inst ("_" ^ i') in
|
|
| 1295 |
pp_static_declare_instance ~ghost macro const_locals fmt (path, m'))) |
|
| 1295 | 1296 |
m.minstances |
| 1296 | 1297 |
|
| 1297 | 1298 |
let pp_static_link_instance ?(ghost = false) fmt (i, (m, _)) = |
| ... | ... | |
| 1305 | 1306 |
in |
| 1306 | 1307 |
fprintf |
| 1307 | 1308 |
fmt |
| 1308 |
"@[<v>@[<v 2>#define %a(%s) do {\\@,%a%a;\\@]@,} while (0)@]"
|
|
| 1309 |
"@[<v>@[<v 2>#define %a(%s) do {\\@,\
|
|
| 1310 |
@[<h>%a%a;\\@]@]@,} while (0)@]" |
|
| 1309 | 1311 |
(pp_machine_static_link_name ~ghost) |
| 1310 | 1312 |
m.mname.node_id |
| 1311 | 1313 |
inst |
| ... | ... | |
| 1327 | 1329 |
~pp_open_box:pp_open_vbox0 |
| 1328 | 1330 |
~pp_sep:(pp_print_endcut ";\\") |
| 1329 | 1331 |
(fun fmt (i', m') -> |
| 1330 |
let path = sprintf "%s ## _%s" inst i' in
|
|
| 1332 |
let path = concat inst ("_" ^ i') in
|
|
| 1331 | 1333 |
fprintf |
| 1332 | 1334 |
fmt |
| 1333 | 1335 |
"%a;\\@,%s.%s = %s%s" |
| ... | ... | |
| 1342 | 1344 |
let pp_static_alloc_macro ?(ghost = false) fmt (m, attr, inst) = |
| 1343 | 1345 |
fprintf |
| 1344 | 1346 |
fmt |
| 1345 |
"@[<v>@[<v 2>#define %a(%s, %a%s)\\@,%a(%s, %a%s);\\@,%a(%s);@]@]" |
|
| 1347 |
"@[<v>@[<v 2>@[<h>#define %a(%s, %a%s)\\@]@,\ |
|
| 1348 |
@[<h>%a(%s, %a%s);\\@]@,\ |
|
| 1349 |
@[<h>%a(%s);@]@]@]" |
|
| 1346 | 1350 |
(pp_machine_static_alloc_name ~ghost) |
| 1347 | 1351 |
m.mname.node_id |
| 1348 | 1352 |
attr |
| 1349 | 1353 |
(pp_print_list |
| 1354 |
~pp_open_box:pp_open_hbox |
|
| 1350 | 1355 |
~pp_sep:pp_print_comma |
| 1351 | 1356 |
~pp_eol:pp_print_comma |
| 1352 | 1357 |
(pp_c_var_read m)) |
| ... | ... | |
| 1356 | 1361 |
m.mname.node_id |
| 1357 | 1362 |
attr |
| 1358 | 1363 |
(pp_print_list |
| 1364 |
~pp_open_box:pp_open_hbox |
|
| 1359 | 1365 |
~pp_sep:pp_print_comma |
| 1360 | 1366 |
~pp_eol:pp_print_comma |
| 1361 | 1367 |
(pp_c_var_read m)) |
| src/backends/C/c_backend_makefile.ml | ||
|---|---|---|
| 53 | 53 |
[] |
| 54 | 54 |
deps |
| 55 | 55 |
|
| 56 |
let fprintf_dependencies fmt (deps : dep_t list) =
|
|
| 56 |
let fprintf_dependencies arrow_suffix fmt deps =
|
|
| 57 | 57 |
(* eprintf "Deps: %a@." pp_deps dep; *) |
| 58 | 58 |
let compiled_deps = compiled_dependencies deps in |
| 59 | 59 |
|
| ... | ... | |
| 63 | 63 |
Log.report ~level:1 (fun fmt -> fprintf fmt "Adding dependency: %s@." s); |
| 64 | 64 |
fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
|
| 65 | 65 |
("${INC}/io_frontend.c"
|
| 66 |
:: sprintf "${INC}/arrow%s.c" arrow_suffix
|
|
| 66 | 67 |
:: (* IO functions when a main function is computed *) |
| 67 | 68 |
List.map |
| 68 | 69 |
(fun dep -> |
| ... | ... | |
| 74 | 75 |
module type MODIFIERS_MKF = sig |
| 75 | 76 |
(* dep was (bool * ident * top_decl list) *) |
| 76 | 77 |
val other_targets : formatter -> string -> string -> dep_t list -> unit |
| 78 |
val pp_print_dependencies: formatter -> dep_t list -> unit |
|
| 79 |
val pp_arrow_o: formatter -> unit -> unit |
|
| 77 | 80 |
end |
| 78 | 81 |
|
| 79 | 82 |
module EmptyMod : MODIFIERS_MKF = struct |
| 80 | 83 |
let other_targets _ _ _ _ = () |
| 84 |
let pp_print_dependencies = fprintf_dependencies "" |
|
| 85 |
let pp_arrow_o fmt () = pp_print_string fmt "arrow.o" |
|
| 81 | 86 |
end |
| 82 | 87 |
|
| 83 | 88 |
module Main = |
| ... | ... | |
| 127 | 132 |
basename; |
| 128 | 133 |
fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;
|
| 129 | 134 |
fprintf fmt "\t${GCC} -I${INC} -I. -c %s_main.c@." basename;
|
| 130 |
fprintf_dependencies fmt dependencies;
|
|
| 135 |
Mod.pp_print_dependencies fmt dependencies;
|
|
| 131 | 136 |
fprintf |
| 132 | 137 |
fmt |
| 133 |
"\t${GCC} -o ${BINNAME} io_frontend.o %a %s.o %s_main.o %a@."
|
|
| 138 |
"\t${GCC} -o ${BINNAME} io_frontend.o %a %a %s.o %s_main.o %a@."
|
|
| 139 |
Mod.pp_arrow_o () |
|
| 134 | 140 |
(pp_print_list (fun fmt dep -> fprintf fmt "%s.o" dep.name)) |
| 135 | 141 |
(compiled_dependencies dependencies) |
| 136 | 142 |
basename |
| src/backends/C/c_backend_makefile.mli | ||
|---|---|---|
| 4 | 4 |
|
| 5 | 5 |
module type MODIFIERS_MKF = sig |
| 6 | 6 |
val other_targets : formatter -> string -> string -> dep_t list -> unit |
| 7 |
val pp_print_dependencies: formatter -> dep_t list -> unit |
|
| 8 |
val pp_arrow_o: formatter -> unit -> unit |
|
| 7 | 9 |
end |
| 8 | 10 |
|
| 9 | 11 |
module EmptyMod : MODIFIERS_MKF |
| ... | ... | |
| 12 | 14 |
val pp_makefile : string -> string -> dep_t list -> formatter -> unit |
| 13 | 15 |
end |
| 14 | 16 |
|
| 15 |
val fprintf_dependencies : formatter -> dep_t list -> unit |
|
| 17 |
val fprintf_dependencies : string -> formatter -> dep_t list -> unit
|
|
| 16 | 18 |
|
| 17 | 19 |
val compiled_dependencies : dep_t list -> dep_t list |
| 18 | 20 |
|
| src/backends/C/c_backend_spec.ml | ||
|---|---|---|
| 1768 | 1768 |
(**************************************************************************) |
| 1769 | 1769 |
|
| 1770 | 1770 |
module MakefileMod = struct |
| 1771 |
let pp_print_dependencies = C_backend_makefile.fprintf_dependencies "_spec" |
|
| 1772 |
|
|
| 1773 |
let pp_arrow_o fmt () = pp_print_string fmt "arrow_spec.o" |
|
| 1774 |
|
|
| 1771 | 1775 |
let other_targets fmt basename _nodename dependencies = |
| 1772 | 1776 |
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@."; |
| 1773 | 1777 |
(* EACSL version of library file . c *) |
| ... | ... | |
| 1812 | 1816 |
"\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@."
|
| 1813 | 1817 |
basename; |
| 1814 | 1818 |
(* compiling instrumented lib + main *) |
| 1815 |
C_backend_makefile.fprintf_dependencies fmt dependencies;
|
|
| 1819 |
pp_print_dependencies fmt dependencies;
|
|
| 1816 | 1820 |
fprintf |
| 1817 | 1821 |
fmt |
| 1818 | 1822 |
"\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s \
|
Also available in: Unified diff
fix tests procedure