diff --git a/res/universal/res/c/math.h b/res/universal/res/c/math.h
index 6f40141252..d2a9170f00 100644
--- 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);