File tree Expand file tree Collapse file tree 1 file changed +9
-4
lines changed Expand file tree Collapse file tree 1 file changed +9
-4
lines changed Original file line number Diff line number Diff line change @@ -12,23 +12,28 @@ function unix_setitimer(which, newval) {
1212}
1313
1414//Provides: unix_times
15+ //only used for timing statistics in Goblint
1516function unix_times ( x ) {
16- return x ;
17+ return 0 ;
1718}
1819
1920//Provides: max_float
21+ //from Goblint specific stubs for C float operations
2022function max_float ( x ) {
21- return x ;
23+ return Number . MAX_VALUE ;
2224}
2325
2426//Provides: smallest_float
27+ //from Goblint specific stubs for C float operations
28+ //returns the smallest positive and normalized float
2529function smallest_float ( x ) {
26- return x ;
30+ return 2.2250738585072014e-308 ;
2731}
2832
2933//Provides: ml_z_of_int
34+ //Requires: ml_z_of_int64, ml_z_to_int64
3035function ml_z_of_int ( x ) {
31- return x | 0 ;
36+ return ml_z_of_int64 ( ml_z_to_int64 ( x ) ) ;
3237}
3338
3439//Provides: caml_thread_initialize const
You can’t perform that action at this time.
0 commit comments