package goblint-cil

You can search for identifiers within the package.

in-package search v0.2.0

A front-end for the C programming language that facilitates program analysis and transformation

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

Maintainers

Sources

goblint-cil-2.0.6.tbz

sha256=5577007bfac63c3f0609abdb74119fe674c9bc8529d790e90ef73a85964aa07a

sha512=f1a393fa92614ceaf857bec4df474d3e152c578d0ab5fdf791e9129668861ccaa37efae2f18aa539965d6c2ed4dabb47b4a5262aab55112e181935def06f18da

doc/src/goblint-cil/machdepenv.ml.html

Source file `machdepenv.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
open Machdep
module R = Str
module L = List
module H = Hashtbl

let preparse (s:string) : (string, string list) H.t =
  let specTable = H.create 32 in
  let commaRegexp = R.regexp "," in
  let spaceRegexp = R.regexp "[ \t]+" in
  let specRegexp = R.regexp "^\\([a-zA-Z_0-9]+\\)[ \t]*=\\(.*\\)$" in
  let specs = R.split spaceRegexp s in
  let addSpec spec =
    if R.string_match specRegexp spec 0 then begin
      let name = R.matched_group 1 spec in
      let value = R.matched_group 2 spec in
      H.add specTable name (R.split commaRegexp value)
    end
    else
      raise (Failure ("invalid specification string " ^ spec))
  in
  L.iter addSpec specs;
  specTable

let errorWrap name f =
  try
    f name
  with Not_found -> raise (Failure (name ^ " not specified"))
  | _ -> raise (Failure ("invalid format for " ^ name))

let getNthString n specTable name =
  let l = H.find specTable name in
  L.nth l n

let getNthInt n specTable name =
  errorWrap name (fun name -> int_of_string (getNthString n specTable name))

let getNthBool n specTable name =
  errorWrap name (fun name -> bool_of_string (getNthString n specTable name))

let getBool = getNthBool 0
let getInt = getNthInt 0
let getSizeof = getNthInt 0
let getAlignof = getNthInt 1

let respace = Str.global_replace (Str.regexp "_") " "

let modelParse (s:string) : mach =
  let entries =
    try
      preparse s
    with Failure msg -> raise (Failure msg)
    | _ -> raise (Failure "invalid machine specification")
  in
  {
    version_major = 0;
    version_minor = 0;
    version = "machine model " ^ s;
    underscore_name = getBool entries "underscore_name";
    sizeof_short = getSizeof entries "short";
    alignof_short = getAlignof entries "short";
    sizeof_bool = getSizeof entries "bool";
    alignof_bool = getAlignof entries "bool";
    sizeof_int = getSizeof entries "int";
    alignof_int = getAlignof entries "int";
    sizeof_long = getSizeof entries "long";
    alignof_long = getAlignof entries "long";
    sizeof_longlong = getSizeof entries "long_long";
    alignof_longlong = getAlignof entries "long_long";
    sizeof_ptr = getSizeof entries "pointer";
    alignof_ptr = getAlignof entries "pointer";
    alignof_enum = getInt entries "alignof_enum";
    sizeof_float = getSizeof entries "float";
    alignof_float = getAlignof entries "float";
    sizeof_float32x = getSizeof entries "float32x";
    alignof_float32x = getAlignof entries "float32x";
    sizeof_float64x = getSizeof entries "float64x";
    alignof_float64x = getAlignof entries "float64x";
    sizeof_floatcomplex = getSizeof entries "float_complex";
    alignof_floatcomplex = getAlignof entries "float_complex";
    sizeof_double = getSizeof entries "double";
    alignof_double = getAlignof entries "double";
    sizeof_doublecomplex = getSizeof entries "double_complex";
    alignof_doublecomplex = getAlignof entries "double_complex";
    sizeof_longdouble = getSizeof entries "long_double";
    alignof_longdouble = getAlignof entries "long_double";
    sizeof_float128 = getSizeof entries "float128";
    alignof_float128 = getAlignof entries "float128";
    sizeof_longdoublecomplex = getSizeof entries "long_double_complex";
    alignof_longdoublecomplex = getAlignof entries "long_double_complex";
    sizeof_float128complex = getSizeof entries "float128_complex";
    alignof_float128complex = getAlignof entries "float128_complex";
    sizeof_void = getSizeof entries "void";
    sizeof_fun = getSizeof entries "fun";
    alignof_fun = getAlignof entries "fun";
    alignof_str = getInt entries "alignof_string";
    alignof_aligned = getInt entries "max_alignment";
    size_t = respace (getNthString 0 entries "size_t");
    wchar_t = respace (getNthString 0 entries "wchar_t");
    char16_t = respace (getNthString 0 entries "char16_t");
    char32_t = respace (getNthString 0 entries "char32_t");
    char_is_unsigned = not (getBool entries "char_signed");
    little_endian = not (getBool entries "big_endian");
    __thread_is_keyword = getBool entries "__thread_is_keyword";
    __builtin_va_list = getBool entries "__builtin_va_list";
  }