Project

General

Profile

« Previous | Next » 

Revision 5500edb8

Added by Pierre-Loïc Garoche over 6 years ago

  • ID 5500edb8f813bab0dbb16ea658a9451bc75add7f
  • Parent 9b04601c

Two fresh branches :)
to manage enum and arrays in the horn backend.

View differences:

src/machine_code.ml
30 30
  | Access of value_t * value_t
31 31
  | Power of value_t * value_t
32 32

  
33
let rec get_array_instr_multidim e =
34
  let res =  
35
    match e with
36
  | Cst c -> get_array_const_multidim c
37
  | LocalVar v | StateVar v -> Types.multidim v.var_type
38
  | Fun _ -> 0 (* basic function, ie. no array manipulation *)
39
  | Array (vl_hd::_) -> 1 + (get_array_instr_multidim vl_hd)
40
  | Array [] -> assert false
41
  | Access (arr, _) -> -1 + (get_array_instr_multidim arr)
42
  | Power (e, _) -> 1 + (get_array_instr_multidim e)
43
  in
44
  if res < 0 then
45
    assert false (* Just to make sure we are not computing negative multi-dimension *)
46
  else
47
    res
48

  
33 49
type instr_t =
34 50
  | MLocalAssign of var_decl * value_t
35 51
  | MStateAssign of var_decl * value_t

Also available in: Unified diff