ispras / cv

Klever Continuous Verification Framework
Apache License 2.0
1 stars 3 forks source link

Support CIF comments #62

Closed mutilin closed 4 months ago

mutilin commented 8 months ago
  1. /* CIF Original function "kzalloc". Instrumenting function "kzalloc". */ is replaced by Instrumented function 'kzalloc' in visualization

  2. LDV model 'kzalloc' - where it comes from?

vmordan commented 4 months ago

Example of error trace:

    835                        cif_spin_unlock_irqrestore_lock_of_garmin_data
    955                          ldv_spin_unlock_lock_of_garmin_data
    306                            Cut all infeasible paths
    308                            Unlock spinlock "lock_of_garmin_data"

But here we would like to see spin_unlock_irqrestore instead due to:

 951 /* CIF Original function "spin_unlock_irqrestore". Instrumenting function "cif_spin_unlock_irqrestore_lock_of_garmin_data". */
 952 __attribute__((gnu_inline)) static inline void cif_spin_unlock_irqrestore_lock_of_garmin_data (spinlock_t *lock, long unsigned int flags)
 953 {
 954 
 955  ldv_spin_unlock_lock_of_garmin_data();
 956 
 957   spin_unlock_irqrestore(lock, flags);
 958 }