goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
136 stars 20 forks source link

`joinLoc` for different filenames #55

Closed vogler closed 2 years ago

vogler commented 2 years ago

Fix #54.

vogler commented 2 years ago

Just returning the left location does not work:

fd-reopen.c:34: Error: Cannot resolve variable tmp.
Error: There were errors during merging

Fatal error: exception Errormsg.Error
Raised at Errormsg.s in file "src/ocamlutil/errormsg.ml" (inlined), line 49, characters 17-28
Called from Cilfacade.getMergedAST in file "src/util/cilfacade.ml", line 153, characters 4-54
Called from Maingoblint.merge_preprocessed in file "src/maingoblint.ml", line 310, characters 12-37
Called from Maingoblint.main in file "src/maingoblint.ml", line 505, characters 15-56
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 554, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 560, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20
vogler commented 2 years ago

Removing the filename equality checks gives the same result.

sim642 commented 2 years ago

Just returning the left location does not work:

This should work because returning l1 is just as good as it was before #51, only having start locations.

The first error there is

/usr/include/bits/stdlib.h:46: Error: Invalid position for (prefix) function type attributes: __attribute__((__warn_unused_result__,
__artificial__)) 

which seems related to #52, where some support for some attribute placement was removed.

sim642 commented 2 years ago

Actually, I'm not even sure if it's related to #52, because the code in question is this:

#line 46
    return ((char __attribute__((__warn_unused_result__, __artificial__))  *)tmp___0);

Both of those attributes are for functions, but there's no function here at all, so it's actually not even valid to use these attributes in this type. How has this ever worked?

EDIT: GCC currently just warns about this:

/usr/include/bits/stdlib.h:46:5: warning: ‘warn_unused_result’ attribute only applies to function types [-Wattributes]
/usr/include/bits/stdlib.h:46:5: warning: ‘artificial’ attribute does not apply to types [-Wattributes]

I don't know that we've ever made CIL more strict about this though.

It looks like maybe the merging process has incorrectly put copied these attributes there when forcing a cast to the function return type:

__inline extern char __attribute__((__warn_unused_result__, __artificial__))  *( __attribute__((__always_inline__)) realpath)(char const   * __restrict  __name ,
                                                                                                                              char * __restrict  __resolved ) 

It's just that those attributes are for the function, not the type.

sim642 commented 2 years ago

I opened a new PR #56 which allows cksum_comb.c at least to be parsed and analyzed, so I'll close this.