|
1 | 1 | open OUnit2 |
2 | 2 |
|
3 | 3 | let memset_desc: LibraryDesc.t = LibraryDsl.( |
4 | | - unknown [drop "dest" [w]; drop "ch" []; drop "count" []] |
5 | | -) |
| 4 | + unknown [drop "dest" [w]; drop "ch" []; drop "count" []] |
| 5 | + ) |
6 | 6 |
|
7 | 7 | let pthread_mutex_lock_desc: LibraryDesc.t = LibraryDsl.( |
8 | | - special [__' [r]] @@ fun e -> Lock { lock = e; try_ = false; write = true; return_on_success = false; } (* actual description in LibraryFunctions has try_ depending on sem.lock.fail *) |
9 | | -) |
| 8 | + special [__' [r]] @@ fun e -> Lock { lock = e; try_ = false; write = true; return_on_success = false; } (* actual description in LibraryFunctions has try_ depending on sem.lock.fail *) |
| 9 | + ) |
10 | 10 |
|
11 | 11 | let pthread_create_desc: LibraryDesc.t = LibraryDsl.( |
12 | | - special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [r]; __ "arg" [r]] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg } |
13 | | -) |
| 12 | + special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [r]; __ "arg" [r]] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg } |
| 13 | + ) |
14 | 14 |
|
15 | 15 | let realloc_desc: LibraryDesc.t = LibraryDsl.( |
16 | | - special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size } |
17 | | -) |
| 16 | + special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size } |
| 17 | + ) |
18 | 18 |
|
19 | 19 | let scanf_desc': LibraryDesc.t = LibraryDsl.( |
20 | | - special ((drop "format" []) :: VarArgs (__' [w])) @@ fun (args: Cil.exp list) -> Unknown |
21 | | -) |
| 20 | + special ((drop "format" []) :: VarArgs (__' [w])) @@ fun (args: Cil.exp list) -> Unknown |
| 21 | + ) |
22 | 22 |
|
23 | 23 | let scanf_desc: LibraryDesc.t = LibraryDsl.( |
24 | | - unknown ((drop "format" []) :: VarArgs (drop' [w])) |
25 | | -) |
| 24 | + unknown ((drop "format" []) :: VarArgs (drop' [w])) |
| 25 | + ) |
26 | 26 |
|
27 | 27 | let rand_desc: LibraryDesc.t = LibraryDsl.( |
28 | | - unknown ~attrs:[ThreadUnsafe] [] |
29 | | -) |
| 28 | + unknown ~attrs:[ThreadUnsafe] [] |
| 29 | + ) |
30 | 30 |
|
31 | 31 | (* this file currently only tests that the above DSL usage compiles *) |
32 | 32 | (* TODO: runtime tests *) |
|
0 commit comments