summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-30 15:06:20 +0000
committerAlasdair Armstrong2018-01-30 15:11:14 +0000
commit368e8b200d53611ca145c63a876a6d37fcf5acaf (patch)
tree561d0ef1bbcf8d0c650e846f10a9b00f303c532c /src/process_file.ml
parent2a14c291caa7b07ac1e3ed6904765ea8702a4818 (diff)
Fix failing Lem tests
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index 1ba8069f..8f75c7a3 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -93,7 +93,7 @@ let cond_pragma defs =
else
else_defs := (def :: !else_defs)
in
-
+
let rec scan = function
| Parse_ast.DEF_pragma ("endif", _, _) :: defs when !depth = 0 ->
(List.rev !then_defs, List.rev !else_defs, defs)
@@ -108,13 +108,13 @@ let cond_pragma defs =
| [] -> failwith "$ifdef or $ifndef never ended"
in
scan defs
-
+
let rec preprocess = function
| [] -> []
| Parse_ast.DEF_pragma ("define", symbol, _) :: defs ->
symbols := StringSet.add symbol !symbols;
preprocess defs
-
+
| Parse_ast.DEF_pragma ("ifndef", symbol, _) :: defs ->
let then_defs, else_defs, defs = cond_pragma defs in
if not (StringSet.mem symbol !symbols) then
@@ -128,7 +128,7 @@ let rec preprocess = function
preprocess (then_defs @ defs)
else
preprocess (else_defs @ defs)
-
+
| Parse_ast.DEF_pragma ("include", file, l) :: defs ->
let len = String.length file in
if len = 0 then
@@ -151,18 +151,18 @@ let rec preprocess = function
let file = Filename.concat sail_dir ("lib/" ^ file) in
let (Parse_ast.Defs include_defs) = parse_file file in
let include_defs = preprocess include_defs in
- include_defs @ preprocess defs
+ include_defs @ preprocess defs
else
let help = "Make sure the filename is surrounded by quotes or angle brackets" in
(Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess defs)
| Parse_ast.DEF_pragma (p, arg, _) :: defs ->
- (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs)
-
+ (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs)
+
| def :: defs -> def :: preprocess defs
let preprocess_ast (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess defs)
-
+
let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs
let load_file_no_check order f = convert_ast order (preprocess_ast (parse_file f))