Revision 4240dfcb
Added by LĂ©lio Brun 10 months ago
src/backends/C/c_backend_spec.ml  

1849  1849 
fprintf fmt "@." 
1850  1850 
end 
1851  1851  
1852 
(* TODO: complete this list *) 

1853 
let acsl_keywords = ISet.of_list ["set"] 

1854  
1855 
let sanitize x = if ISet.mem x acsl_keywords then "__" ^ x else x 

1856  
1857 
let sanitize_var_decl vd = { vd with var_id = sanitize vd.var_id } 

1858  
1859 
let sanitize_var_decls = List.map sanitize_var_decl 

1860  
1861 
let rec sanitize_value v = 

1862 
let value_desc = match v.value_desc with 

1863 
 Machine_code_types.Var vd > Machine_code_types.Var (sanitize_var_decl vd) 

1864 
 Fun (f, vs) > Fun (f, sanitize_values vs) 

1865 
 Array vs > Array (sanitize_values vs) 

1866 
 Access (v1, v2) > Access (sanitize_value v1, sanitize_value v2) 

1867 
 Power (v1, v2) > Power (sanitize_value v1, sanitize_value v2) 

1868 
 v > v 

1869 
in 

1870 
{ v with value_desc } 

1871  
1872 
and sanitize_values vs = List.map sanitize_value vs 

1873  
1874 
let sanitize_expr = function 

1875 
 Val v > Val (sanitize_value v) 

1876 
 Var v > Var (sanitize_var_decl v) 

1877 
 e > e 

1878  
1879 
let sanitize_predicate = function 

1880 
 Transition (st, f, inst, i, vs, r, mf, mfinsts) > 

1881 
Transition (st, f, inst, i, List.map sanitize_expr vs, r, mf, mfinsts) 

1882 
 p > p 

1883  
1884 
let rec sanitize_formula = function 

1885 
 Equal (e1, e2) > Equal (sanitize_expr e1, sanitize_expr e2) 

1886 
 GEqual (e1, e2) > GEqual (sanitize_expr e1, sanitize_expr e2) 

1887 
 And fs > And (sanitize_formulae fs) 

1888 
 Or fs > Or (sanitize_formulae fs) 

1889 
 Imply (f1, f2) > Imply (sanitize_formula f1, sanitize_formula f2) 

1890 
 Exists (vs, f) > Exists (sanitize_var_decls vs, sanitize_formula f) 

1891 
 Forall (vs, f) > Forall (sanitize_var_decls vs, sanitize_formula f) 

1892 
 Ternary (e, t, f) > Ternary (sanitize_expr e, sanitize_formula t, sanitize_formula f) 

1893 
 Predicate p > Predicate (sanitize_predicate p) 

1894 
 ExistsMem (m, f1, f2) > ExistsMem (m, sanitize_formula f1, sanitize_formula f2) 

1895 
 Value v > Value (sanitize_value v) 

1896 
 f > f 

1897  
1898 
and sanitize_formulae fs = List.map sanitize_formula fs 

1899  
1900 
let rec sanitize_instr i = 

1901 
let sanitize_instr_desc = function 

1902 
 MLocalAssign (x, v) > 

1903 
MLocalAssign (sanitize_var_decl x, sanitize_value v) 

1904 
 MStateAssign (x, v) > 

1905 
MStateAssign (x, sanitize_value v) 

1906 
 MStep (xs, f, vs) > 

1907 
MStep (sanitize_var_decls xs, f, sanitize_values vs) 

1908 
 MBranch (v, brs) > 

1909 
MBranch (sanitize_value v, List.map (fun (t, instrs) > t, sanitize_instrs instrs) brs) 

1910 
 i > i 

1911 
in 

1912 
{ i with 

1913 
instr_desc = sanitize_instr_desc i.instr_desc; 

1914 
instr_spec = sanitize_formulae i.instr_spec 

1915 
} 

1916  
1917 
and sanitize_instrs instrs = List.map sanitize_instr instrs 

1918  
1919 
let sanitize_step s = 

1920 
{ s with 

1921 
step_inputs = sanitize_var_decls s.step_inputs; 

1922 
step_outputs = sanitize_var_decls s.step_outputs; 

1923 
step_locals = sanitize_var_decls s.step_locals; 

1924 
step_instrs = sanitize_instrs s.step_instrs 

1925 
} 

1926  
1927 
let sanitize_transition t = 

1928 
{ t with 

1929 
tvars = sanitize_var_decls t.tvars; 

1930 
tformula = sanitize_formula t.tformula 

1931 
} 

1932  
1933 
let sanitize_transitions = List.map sanitize_transition 

1934  
1935 
let sanitize_memory_pack mp = 

1936 
{ mp with 

1937 
mpformula = sanitize_formula mp.mpformula 

1938 
} 

1939  
1940 
let sanitize_memory_packs = List.map sanitize_memory_pack 

1941  
1942 
let sanitize_spec s = 

1943 
{ s with 

1944 
mtransitions = sanitize_transitions s.mtransitions; 

1945 
mmemory_packs = sanitize_memory_packs s.mmemory_packs 

1946 
} 

1947 
let sanitize_machine m = 

1948 
{ m with 

1949 
mstep = sanitize_step m.mstep; 

1950 
mspec = sanitize_spec m.mspec 

1951 
} 

1952  
1953 
let sanitize_machines = List.map sanitize_machine 

1954  
1852  1955 
(* Local Variables: *) 
1853  1956 
(* compilecommand:"make C ../../.." *) 
1854  1957 
(* End: *) 
Also available in: Unified diff
add basic support to protect against some ACSL keywords