Add fabs again

sakehl · May 6, 2024 · e438c7b · e438c7b
1 parent 8b621c8
commit e438c7b
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/res/universal/res/c/math.h b/res/universal/res/c/math.h
@@ -8,6 +8,12 @@
 pure double M_PI() = 3.14159265358979323846;
 @*/
 
+/*@
+  ensures \result == (x >= 0 ? x : -x);
+  decreases;
+@*/
+float /*@ pure @*/ fabsf(float x);
+
 /*@
   requires x>= 0;
   ensures \result == \pow(x, 0.5);
@@ -118,6 +124,12 @@ float /*@ pure @*/ ceilf(float x);
 @*/
 float /*@ pure @*/ roundf(float x);
 
+/*@
+  ensures \result == (x >= 0 ? x : -x);
+  decreases;
+@*/
+double /*@ pure @*/ fabs(double x);
+
 /*@
   requires x>= 0;
   ensures \result == pow(x, 0.5);