Linux Driver Verification » BLAST

BLAST calculates aliases of return as assignments of the "return value" (BLAST uses CIL transformation that makes functions have only one exit point that returns a specific value) to the recipient at caller's site.

However, it doesn't seem to correctly get the return lval of the function. Let's see the code in Alias Analyzer:

(* get the assignment for retval *)                                                                   
let returnlvalue = Expression.Lval(Expression.Symbol("__retres@"^fname)) in                           
let new_bdd_at_target = do_assignment true new_bdd_at_entry_loc retval returnlvalue in                
  new_bdd_at_target

However, the return values do not fall under this pattern. Sometimes, the special lvalues are not generated (if the function is simple), and the statements look simply as Return(p@return_self). Or, they have a number after __retres, as in Return(__retres3@main).

The relevant test (alias_of_return.c) is added to the regression test set.

Should be fixed, as it's important for seamless processing of dev_get_drvdata function.