File tree Expand file tree Collapse file tree 1 file changed +6
-6
lines changed Expand file tree Collapse file tree 1 file changed +6
-6
lines changed Original file line number Diff line number Diff line change 3
3
4
4
extern int __CPROVER_rounding_mode ;
5
5
6
- void __asm_fnstcw (unsigned short * dest )
6
+ void __asm_fnstcw (void * dest )
7
7
{
8
8
// the rounding mode is bits 10 and 11 in the control word
9
- * dest = __CPROVER_rounding_mode << 10 ;
9
+ * ( unsigned short * ) dest = __CPROVER_rounding_mode << 10 ;
10
10
}
11
11
12
12
/* FUNCTION: __asm_fstcw */
13
13
14
14
extern int __CPROVER_rounding_mode ;
15
15
16
- void __asm_fstcw (unsigned short * dest )
16
+ void __asm_fstcw (void * dest )
17
17
{
18
18
// the rounding mode is bits 10 and 11 in the control word
19
- * dest = __CPROVER_rounding_mode << 10 ;
19
+ * ( unsigned short * ) dest = __CPROVER_rounding_mode << 10 ;
20
20
}
21
21
22
22
/* FUNCTION: __asm_fldcw */
23
23
24
24
extern int __CPROVER_rounding_mode ;
25
25
26
- void __asm_fldcw (const unsigned short * src )
26
+ void __asm_fldcw (void * src )
27
27
{
28
28
// the rounding mode is bits 10 and 11 in the control word
29
- __CPROVER_rounding_mode = ((* src )>> 10 )& 3 ;
29
+ __CPROVER_rounding_mode = ((* ( const unsigned short * ) src ) >> 10 ) & 3 ;
30
30
}
31
31
32
32
/* FUNCTION: __asm_mfence */
You can’t perform that action at this time.
0 commit comments