Objects.qll has support for identifying objects with different storage durations (static, thread local, allocated, and automatic). However, its thread local object support is limited to _Thread_local variables.
Ideally, a tss_t variable would be recognizable as two objects:
- One object representing the variable holding the tss_t key. Usually this is an object with static lifetime.
- Another object identity for the thread local behind the
tss_t.
Unfortunately, tss_t currently extends Element, which means that it can't have two implementations of the ObjectIdentity class. Alternatively, calls to tss_get() could be considered ObjectIdentitys, however, that doesn't match the intention of the ObjectIdentity class/library, as the threadlocal is really identified by the tss_t.
The threadlocal object could be identified by the tss_create call (similarly to how we identify dynamic memory via malloc calls). But it probably makes more sense to have ObjectIdentity extend Locatable and then have a tss_t variable produce two ObjectIdentys.
Otherwise the tss_t object class will closely match the malloc object class, since malloc returns a pointer to the dynamic memory just like tss_get() returns a pointer to the thread local. Additional refactoring to share code here will be required.
Objects.qllhas support for identifying objects with different storage durations (static, thread local, allocated, and automatic). However, its thread local object support is limited to_Thread_localvariables.Ideally, a
tss_tvariable would be recognizable as two objects:tss_t.Unfortunately,
tss_tcurrently extendsElement, which means that it can't have two implementations of theObjectIdentityclass. Alternatively, calls totss_get()could be consideredObjectIdentitys, however, that doesn't match the intention of theObjectIdentityclass/library, as the threadlocal is really identified by thetss_t.The threadlocal object could be identified by the
tss_createcall (similarly to how we identify dynamic memory viamalloccalls). But it probably makes more sense to haveObjectIdentityextendLocatableand then have atss_tvariable produce twoObjectIdentys.Otherwise the tss_t object class will closely match the malloc object class, since malloc returns a pointer to the dynamic memory just like
tss_get()returns a pointer to the thread local. Additional refactoring to share code here will be required.