RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

conversion: fixed hardcoded spec rule for clzl

Browse Source
This commit is contained in:
Joel Beeren
2015-12-09 17:48:46 +11:00
parent a0c228c953
commit 84fb0dcdfe
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
include/util.h
View File

@@ -78,8 +78,8 @@ long PURE str_to_long(const char* str);
/** FNSPEC clzl_spec:
"\<forall>s. \<Gamma> \<turnstile>
{\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0 }
\<acute>ret__int :== PROC clzl(\<acute>x)
\<lbrace> \<acute>ret__int = of_nat (word_clz (x_' s)) \<rbrace>"
\<acute>ret__long :== PROC clzl(\<acute>x)
\<lbrace> \<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"
*/
static inline long
CONST clzl(unsigned long x)